Step of Proof: gen_hyp_tp
9,38
postcript
pdf
Inference at
*
1
1
3
2
I
of proof for Lemma
gen
hyp
tp
:
.....wf..... NILNIL
1.
A
: Type
2.
e
:
A
3.
H
:
A
Type
4.
H
(
e
)
5.
A
Type
6.
e
A
A
Type
latex
by (SoftNthHyp (-2))
latex
.
origin
Type
Type
A
A Type
by (SoftNthHyp (-2))
.Type
Type
A
A Type
by (SoftNthHyp (-2))
.